Issue1967.agda:5,22-23
Set should be a function type, but it isn't
when checking that A is a valid argument to a function of type
⦃ A = A₁ : Set ⦄ → Set
